$\forall$${\it es}$:ES, $C$, $T$:Type, ${\it In}$:AbsInterface(:(:$C$ $\times$ $C$) $\times$ $T$). abs{-}S  $\in$ $C$$\rightarrow$$C$$\rightarrow$E$\rightarrow\mathbb{P}$